\begin{tabbing}
$\forall$${\it es}$:ES, $x$, $i$:Id, $T$:Type.
\\[0ex]($\forall$$x$, $y$:$T$. Dec($x$ = $y$ $\in$ $T$))
\\[0ex]$\Rightarrow$ @$i$($x$:$T$)
\\[0ex]$\Rightarrow$ \=$\forall$${\it e'}$@$i$.\+
\\[0ex]($\forall$$e$$<$${\it e'}$. ($x$ when $e$) = ($x$ when ${\it e'}$) $\in$ $T$)
\\[0ex]$\vee$ ($\exists$\=$e$:E\+
\\[0ex](($e$ $<$loc ${\it e'}$)
\\[0ex]c$\wedge$ \=(($\neg$(($x$ when $e$) = ($x$ after $e$) $\in$ $T$))\+
\\[0ex]\& ($\forall$${\it e''}$:E. ($e$ $<$loc ${\it e''}$) $\Rightarrow$ ${\it e''}$ $\leq$loc ${\it e'}$  $\Rightarrow$ (($x$ when ${\it e''}$) = ($x$ when ${\it e'}$) $\in$ $T$)))))
\-\-\-
\end{tabbing}